PosetSig\{i\} $\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$${\it car}$:Type\{i\} $\times$ (${\it eq}$:(${\it car}$$\rightarrow$${\it car}$$\rightarrow\mathbb{B}$) $\times$ (${\it car}$$\rightarrow$${\it car}$$\rightarrow\mathbb{B}$))